抽象によるソフトウェア設計 Alloyではじめる形式手法(本)